$\forall$$A$:Realizer.
\\[0ex]Rplus?($A$) $\Rightarrow$ \{R{-}size(Rplus{-}left($A$))$<$R{-}size($A$) \& R{-}size(Rplus{-}right($A$))$<$R{-}size($A$)\}